Nuprl Lemma : ma-valtype_wf
11,40
postcript
pdf
da
:fpf(Knd;
z
.Type),
k
:Knd. ma-valtype(
da
;
k
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
ma-valtype(
da
;
k
)
,
x
.
t
(
x
)
,
x
(
s
)
Lemmas
fpf-cap
wf
,
Knd
wf
,
Kind-deq
wf
,
top
wf
,
fpf
wf
origin
da:fpf(Knd; z.Type), k:Knd. ma-valtype(da; k) 
Type da:fpf(Knd; z.Type), k:Knd. ma-valtype(da; k) Type x:A. B(x) T
x. t(x)